#!/usr/bin/ruby -w

require "test/unit"
require "converter.rb"

# Effectively, if we view the conversion problem from a high level, we can
# distinguish between two types of formulas to be converted. Namely:
# - Formulas that produce that are the same in CNF as in SAT.
# - Formulas that produce are different in CNF than in SAT.
class TestConverter < Test::Unit::TestCase

  def setup
    @converter = FormulaConverter.new
  end

  def test_no_convert_needed
    # !A ^ (B v C)
    example1 = And.new(NegationLiteral.new(1), Or.new(Literal.new(2), Literal.new(3)))
    assert_equal("p cnf 3 2\n-1 0\n2 3\n", @converter.convert_tree(example1).to_s)
    
    # normal: (1 v 3 v !4) ^ (4) ^ (2 v !3)
    # polish: (*( +(1 3 -4) +(4) +(2 3)))
    #
    #              ^
    #           /     \
    #          v       ^
    #         / \     / \
    #        1   v   4   v
    #           / \     / \
    #          3  !4   2  !3
    #
    # (A v C v !D) ^ (D) ^ (B v !C)
    example2 = And.new(Or.new(Literal.new(1), Or.new(Literal.new(3), NegationLiteral.new(4))), 
                       And.new(Literal.new(4), Or.new(Literal.new(2), NegationLiteral.new(3))))
    assert_equal("p cnf 4 3\n1 3 -4 0\n4 0\n2 -3\n", @converter.convert_tree(example2).to_s)
  end
  
  def test_convert_not_cnf_to_cnf
    # (A ^ B) v C   =>   !B ^ !C
    example1 = Or.new(And.new(Literal.new(1), Literal.new(2)), Literal.new(3))
    assert_equal("p cnf 3 2\n1 3 0\n2 3\n", @converter.convert_tree(example1).to_s)
    
    # A ^ (B v (D ^ E))   =>   A ^ (B v D) ^ (B v E)
    example2 = And.new(Literal.new(1), Or.new(Literal.new(2), And.new(Literal.new(4), Literal.new(5))))
    assert_equal("p cnf 4 3\n1 0\n2 4 0\n2 5\n", @converter.convert_tree(example2).to_s)
  end
end

# Indication of time spent: 16 hours. Most time spent on using the very
# unfriendly parser generator 'Treetop' and alternatively on RegExing our way
# through the parsing of the SAT syntax.
